Nuprl Lemma : select_l_index
0,22
postcript
pdf
T
:Type,
dT
:EqDecider(
T
),
L
:
T
List,
x
:
T
. (
x
L
)
L
[index(
L
;
x
)] =
x
latex
Definitions
mu(
f
)
,
A
&
B
,
i
j
<
k
,
P
Q
,
P
Q
,
||
as
||
,
eqof(
d
)
,
l
[
i
]
,
index(
L
;
x
)
,
{
T
}
,
,
A
B
,
A
,
False
,
i
j
,
x
:
A
.
B
(
x
)
,
b
,
{
i
..
j
}
,
P
&
Q
,
P
Q
,
(
x
l
)
,
EqDecider(
T
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
deq
wf
,
l
member
wf
,
int
seg
wf
,
select
wf
,
eqof
wf
,
length
wf1
,
non
neg
length
,
mu-bound-property
,
deq
property
,
le
wf
,
assert
wf
,
nat
wf
,
mu
wf
,
l
index
wf
origin
T:Type, dT:EqDecider(T), L:T List, x:T. (x 
L) 
L[index(L;x)] = x T:Type, dT:EqDecider(T), L:T List, x:T. (x L) L[index(L;x)] = x 
j < k
Q Q
B
A
j
x:A. B(x)
b
} Q l)x:A. B(x) T